n, m:, f:(nm), x1, x2:n, y1, y2:m.
x1 = x2    y1 = y2  
 (x:n, y:m. (x = x1   & y = y1  )  (x = x2   & y = y2  )  f(x,y) = 0)
 sum(f(x,y) | x < n; y < m) = f(x1,y1)+f(x2,y2) 

latex

Definitions	i  j < k, AB, False, P  Q, P & Q, x(s1,s2), A, Prop, {i..j}, t  T, , sum(f(x;y) | x < n; y < m), x:A. B(x), Dec(P), P  Q, sum(f(x) | x < k), x. t(x), x(s), SQType(T), {T}
Lemmas	pair support, empty support, sum wf, singleton support sum, decidable int equal, nat wf, int seg wf, not wf